COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	term	::= var
C00003 00003	unify[x:termsy:termsz:subs]answer
C00005 ENDMK
C⊗;
term	::= var
	::= f_app

f_app	::= struct[n:f_name;a:terms]

f_name	::= id

terms	::= seq[term]

subs	::= seq[sub]

sub	::= struct[n:var;v:term]

answer	::= boolean
	::= subs
unify[x:terms;y:terms;z:subs]answer
 on(x,y;ε,λ[[r,t,z]{generic(unify1(r,t,z))
			[boolean] → FALSE}])       *"→" means exit with value
			

unify1[t:term;u:term;z:subs]answer
 generic(a:subst(t,z),b:subst(u,z))
	[var,var] => compose(z,a,b)
	[var,f_app(*,c)] => {occ_list(a,c) => FALSE;compose(z,a,c)}
	[f_app(*,c),var] => {occ_list(b,c) => FALSE;compose(z,b,c)}
	[f_app(f,c),f_app(g,d)] => {f≠g => FALSE;unify(c,d,z)}
 end;

subst[t:term;z;subs]term
 generic(t)
	[var] => subv(t,z)
	[f_app(u,v)] => f_app(u,su_list(v,z))
 end;

subv[x:var;z;subs]term
 on(z;x,λ[[z,y] n(z)=x → v(z)])

su_list[x;terms;z:subs]terms
 on(x; *,λ[[x,y]subst(x,z)]; ε,terms)

occur[x:var;t:term]boolean
 generic(t)
	[var] =>x=t
	[f_app(*,v)] => occ_list(x,v)
 end;

occ_list(x:var;y:terms) boolean
 on(y; FALSE,λ[[y,z][occur(x,y)→TRUE]])

compose[z:subs;v:var;t:term]subs
 on(z;ε,λ[[u,w][n(u)=v → LOSS; sub(u,subst(a,subs(sub(v,t))))]];sub(v,t),subs)
 end;